;;; -*- Mode: LISP; Package: USER; Base: 10 -*-

(HERALD PPR)

;   In order to speed up theorem-prover output, this pretty-printer is
;   based around PRINC rather than PRIN1 because in Zetalisp, PRIN1
;   has to spend time thinking about whether to add a package prefix.

(DEFUN PPRIND (FMLA LEFTMARGIN RPARCNT PPR-MACRO-LST PPRFILE)
  (PROG (MARG2 PPR-MACRO-MEMO STARTLIST)
	(SETQ MARG2 (LINEL PPRFILE))
	(COND
	  ((ATOM FMLA)
	   (IPRIN1 FMLA PPRFILE)
	   (RETURN NIL)))
        (SETQ POS (COND ((SETQ TEMP-TEMP (ASSQ PPRFILE IPOSITION-ALIST))
			 (CDR TEMP-TEMP))
			(T 0)))
	(SETQ SPACELEFT (- MARG2 LEFTMARGIN))
	(PPR1 FMLA (1+ RPARCNT))
	(SETQ NEXTNODE (CDAR STARTLIST))
	(SETQ NEXTIND (CAAR STARTLIST))
	(SETQ PPR-MACRO-MEMO (NREVERSE PPR-MACRO-MEMO))
	(SETQ NEXT-MEMO-KEY (CAAR PPR-MACRO-MEMO))
	(SETQ NEXT-MEMO-VAL (CDAR PPR-MACRO-MEMO))
	(PPR2 FMLA LEFTMARGIN RPARCNT)
        (IPOSITION PPRFILE POS NIL)
	(RETURN NIL)))

(DEFUN PPRPACK NIL
  (CONS (COND ((< MINREM DLHDFMLA) (SETQ REMAINDER 0) (MINUS (1+ MINREM)))
	      (T (SETQ REMAINDER (- MINREM DLHDFMLA)) (1+ DLHDFMLA)))
	FMLA))

(DEFUN PPR1 (FMLA RPARCNT)
  (LET (DLHDFMLA RUNFLAT MINREM L RUNSTART RUNEND
		 (PPR-MACRO-LST PPR-MACRO-LST))
    (PROG NIL
	  (COND
	   ((ATOM FMLA)
	     (SETQ FLATSIZE (+ RPARCNT
			       (COND ((SYMBOLP FMLA) (STRING-LENGTH FMLA))
				     (T (FLATC FMLA)))))
	     (SETQ REMAINDER (- SPACELEFT FLATSIZE))
	     (RETURN NIL)))
	  (COND
	    ((ATOM (CAR FMLA))
	     (COND
	       ((SETQ TEMP1 (ASSQ (CAR FMLA) PPR-MACRO-LST))
		(SETQ TEMP1 (FUNCALL (CDR TEMP1) FMLA))
		(SETQ PPR-MACRO-MEMO (CONS (CONS FMLA TEMP1) PPR-MACRO-MEMO))
		(COND
		  ((ATOM TEMP1)
		   (SETQ FLATSIZE (+ RPARCNT
				     (COND ((SYMBOLP TEMP1) (STRING-LENGTH TEMP1))
					   (T (FLATC TEMP1)))))
		   (SETQ REMAINDER (- SPACELEFT FLATSIZE))
		   (RETURN NIL))
		  (T (SETQ FMLA TEMP1)))))
	     (COND ((AND (EQ (QUOTE QUOTE) (CAR FMLA))
			 (NOT (ATOM (CDR FMLA)))
			 (NULL (CDDR FMLA)))
		    (PPR1 (CADR FMLA) RPARCNT)
		    (AND FLATSIZE (SETQ FLATSIZE (1+ FLATSIZE)))
		    (SETQ REMAINDER (1- REMAINDER))
		    (RETURN NIL)))
	     (SETQ DLHDFMLA (1+ (COND ((SYMBOLP (CAR FMLA))
				       (STRING-LENGTH (CAR FMLA)))
				      (T (FLATC (CAR FMLA))))))
	     (SETQ L FMLA))
	    (T (SETQ DLHDFMLA 0)
	       (SETQ L (RPLACD NILCONS FMLA))
	       (GO OVER)))
	  (COND
	    ((NULL (CDR FMLA))
	     (SETQ FLATSIZE (+ RPARCNT DLHDFMLA))
	     (SETQ REMAINDER (- SPACELEFT FLATSIZE))
	     (RETURN NIL)))
       OVER
	  (SETQ RUNFLAT DLHDFMLA)
	  (SETQ MINREM 1000)
	  (SETQ SPACELEFT (1- SPACELEFT))
       LOOPFLAT
	  (SETQ L (CDR L))
	  (COND
	    ((NULL L)
	     (SETQ SPACELEFT (1+ SPACELEFT))
	     (COND
	       ((AND (NOT (> RUNFLAT SPACELEFT)) (NOT (> RUNFLAT FORCEIN)))
		(SETQ FLATSIZE RUNFLAT)
		(SETQ REMAINDER (- SPACELEFT RUNFLAT)))
	       (T (SETQ STARTLIST (CONS (PPRPACK) NIL))
		  (SETQ ENDLIST STARTLIST)
		  (SETQ FLATSIZE NIL)))
	     (RETURN NIL)))
	  (COND
	    ((ATOM L)
	     (RPLACA (CDR DOTCONS) L)
	     (SETQ L DOTCONS)))
	  (COND
	    ((ATOM (CAR L))
	     (SETQ TEMP1 (COND ((SYMBOLP (CAR L)) (STRING-LENGTH (CAR L)))
			       (T (FLATC (CAR L)))))
	     (SETQ RUNFLAT (+ TEMP1 (1+ RUNFLAT)))
	     (SETQ TEMP1 (- SPACELEFT TEMP1))
	     (COND
	       ((NULL (CDR L))
		(SETQ RUNFLAT (+ RPARCNT RUNFLAT))
		(SETQ TEMP1 (- TEMP1 RPARCNT))))
	     (COND
	       ((< TEMP1 MINREM)
		(SETQ MINREM TEMP1)))
	     (GO LOOPFLAT))
	    (T (PPR1 (CAR L)
		     (COND
		       ((NULL (CDR L)) (1+ RPARCNT))
		       (T 1)))
	       (COND
		 ((< REMAINDER MINREM) (SETQ MINREM REMAINDER)))
	       (COND
		 (FLATSIZE (SETQ RUNFLAT (+ FLATSIZE (1+ RUNFLAT)))
			   (GO LOOPFLAT)))))
	  (SETQ RUNSTART STARTLIST)
	  (SETQ RUNEND ENDLIST)
       LOOPIND
	  (SETQ L (CDR L))
	  (COND
	    ((NULL L)
	     (SETQ STARTLIST (CONS (PPRPACK) RUNSTART))
	     (SETQ ENDLIST RUNEND)
	     (SETQ FLATSIZE NIL)
	     (SETQ SPACELEFT (1+ SPACELEFT))
	     (RETURN NIL)))
	  (COND
	    ((ATOM L)
	     (RPLACA (CDR DOTCONS) L)
	     (SETQ L DOTCONS)))
	  (COND
	    ((ATOM (CAR L))
	     (SETQ TEMP1 (- SPACELEFT (COND ((SYMBOLP (CAR L))
					     (STRING-LENGTH (CAR L)))
					    (T (FLATC (CAR L))))))
	     (COND
	       ((NULL (CDR L)) (SETQ TEMP1 (- TEMP1 RPARCNT))))
	     (COND
	       ((< TEMP1 MINREM) (SETQ MINREM TEMP1)))
	     (GO LOOPIND)))
	  (PPR1 (CAR L)
		(COND
		  ((NULL (CDR L)) (1+ RPARCNT))
		  (T 1)))
	  (COND
	    ((< REMAINDER MINREM) (SETQ MINREM REMAINDER)))
	  (COND
	    (FLATSIZE)
	    (T (RPLACD RUNEND STARTLIST) (SETQ RUNEND ENDLIST)))
	  (GO LOOPIND))))

(DEFUN PPR2 (FMLA MARG1 RPARCNT)
  (PROG (NONLFLAG TEMP)
    (COND
     ((ATOM FMLA)
      (PRIND FMLA PPRFILE)
      (RETURN NIL)))
    (COND
     ((EQ FMLA NEXT-MEMO-KEY)
      (SETQ FMLA NEXT-MEMO-VAL)
      (SETQ PPR-MACRO-MEMO (CDR PPR-MACRO-MEMO))
      (SETQ NEXT-MEMO-KEY (CAAR PPR-MACRO-MEMO))
      (SETQ NEXT-MEMO-VAL (CDAR PPR-MACRO-MEMO))
      (COND
       ((ATOM FMLA)
	(PRIND FMLA PPRFILE)
	(RETURN NIL)))))
    (COND ((AND (EQ (CAR FMLA) (QUOTE QUOTE))
		(NOT (ATOM (CDR FMLA)))
		(NULL (CDDR FMLA)))
	   (TYO1 #/' PPRFILE)
	   (PPR2 (CADR FMLA) (1+ MARG1) RPARCNT)
	   (RETURN NIL)))
    (COND
     ((EQ FMLA NEXTNODE)
      (SETQ MARG1 (+ MARG1 (ABS NEXTIND)))
      (SETQ NONLFLAG (> NEXTIND 0))
      (SETQ STARTLIST (CDR STARTLIST))
      (COND
       ((NULL STARTLIST))
       (T (SETQ NEXTNODE (CDAR STARTLIST))
	  (SETQ NEXTIND (CAAR STARTLIST)))))
     (T (PPR22 FMLA)
	(RETURN NIL)))
    #+QUANT
    (COND ((EQ (CAR FMLA) (QUOTE ||))
	   (TYO1 MAGIC-CHAR-NO PPRFILE)
	   (SETQ FMLA (CDR FMLA))))
    (TYO1 #/( PPRFILE)
    (COND
     ((ATOM (CAR FMLA))
      (PRIND (CAR FMLA) PPRFILE)
      (COND
       ((NULL (CDR FMLA))
	(TYO1 #/) PPRFILE)
	(RETURN NIL)))
      (COND
       ((AND (PAIRP (CDR FMLA))
	     (OR (ATOM (SETQ TEMP (CADR FMLA)))
		 (AND (NEQ (CADR FMLA) NEXTNODE)
		      (PROGN (COND ((EQ FMLA NEXT-MEMO-KEY)
				    (SETQ TEMP NEXT-MEMO-VAL)))
			     (OR (ATOM TEMP)
				 (AND (EQ (CAR TEMP) (QUOTE QUOTE))
				      (NOT (ATOM (CDR TEMP)))
				      (ATOM (CADR TEMP))
				      (NULL (CDDR TEMP)))))))
	     (< (+ POS (FLATC TEMP) RPARCNT)
		MARG2))
	(TYO1 #\SPACE PPRFILE)
	(PPR2 (CADR FMLA) MARG1 RPARCNT)
	(SETQ FMLA (CDR FMLA))
	(GO LOOP1))
       (NONLFLAG (TYO1 #\SPACE PPRFILE))
       (T (TERPRISPACES MARG1 PPRFILE)))
      (SETQ FMLA (CDR FMLA))))
   LOOP(COND
	((ATOM FMLA)
	 (TYO1 #/. PPRFILE)
	 (TYO1 #\SPACE PPRFILE)
	 (PRIND FMLA PPRFILE)
	 (TYO1 #/) PPRFILE)
	 (RETURN NIL)))
    (PPR2 (CAR FMLA)
	  MARG1
	  (COND
	   ((NULL (CDR FMLA))
	    (1+ RPARCNT))
	   (T 1)))
   LOOP1
    (COND
     ((NULL (CDR FMLA))
      (TYO1 #/) PPRFILE)
      (RETURN NIL)))
    (COND
      ((AND (ATOM (CAR FMLA))
	    (PAIRP (CDR FMLA))
	    (OR (ATOM (SETQ TEMP (CADR FMLA)))
		(AND (NEQ TEMP NEXTNODE)
		     (PROGN (COND ((EQ FMLA NEXT-MEMO-KEY)
				   (SETQ TEMP NEXT-MEMO-VAL)))
			    (OR (ATOM TEMP)
				(AND (EQ (CAR TEMP) (QUOTE QUOTE))
				     (NOT (ATOM (CDR TEMP)))
				     (ATOM (CADR TEMP))
				     (NULL (CDDR TEMP)))))))
	    (< (+ POS (FLATC TEMP) RPARCNT)
	       MARG2))
       (TYO1 #\SPACE PPRFILE)
       (PPR2 (CADR FMLA) MARG2 RPARCNT)
       (SETQ FMLA (CDR FMLA))
       (GO LOOP1)))
    (TERPRISPACES MARG1 PPRFILE)
    (SETQ FMLA (CDR FMLA))
    (GO LOOP)))

(DEFUN PPR22 (X)
  (COND
    ((ATOM X) (PRIND X PPRFILE))
    (T #+QUANT
       (COND ((EQ (CAR X) (QUOTE ||))
	      (TYO1 MAGIC-CHAR-NO PPRFILE)
	      (SETQ X (CDR X))))
       (TYO1 #/( PPRFILE)
       (PROG NIL
	     LOOP (COND
		   ((ATOM X)
		    (COND
		     ((NULL X) (TYO1 #/) PPRFILE))
		     (T (TYO1 #/. PPRFILE)
			(TYO1 #\SPACE PPRFILE)
			(PRIND X PPRFILE)
			(TYO1 #/) PPRFILE)))
		    (RETURN NIL))
		   (T (PPR2 (CAR X) MARG2 0)
		      (SETQ X (CDR X))
		      (COND
		       ((NULL X))
		       (T (TYO1 #\SPACE PPRFILE)))
		      (GO LOOP)))))))

(DEFUN TERPRISPACES (N FILE)
  (TERPRI FILE)
  (LOOP FOR I FROM 1 TO (// N TAB-SIZE) DO (TYO #\TAB FILE))
  (LOOP FOR I FROM 1 TO (\ N TAB-SIZE) DO (TYO #\SPACE FILE))
  (SETQ POS N))